Library fl.int.ChomskyInduction

Require Import List.
Require Import Fin.

Require Import fl.cfg.Binarize.
Require Import fl.cfg.Chomsky.
Require Import fl.cfg.Definitions.
Require Import fl.cfg.Separate.

Module ChomskyInduction.

  Import ListNotations Base Definitions Derivation Chomsky.

  Section Definitions.

    Definition syntactic_analysis_is_possible :=
      ∀ {T V: Type} (G: @grammar T V) (A: var) (l: phrase),
        der G A l →
        (R A l el G) ∨ (∃ rhs, R A rhs el G ∧ derf G rhs l).

  End Definitions.

  Section Induction.

    Context {T V: Type}.

    Variable G: @grammar T V.
    Variable P: @var V → @phrase T V → Prop.

    Hypothesis H_chomsky: chomsky G.
    Hypothesis H_syntactic_analysis: syntactic_analysis_is_possible.

    Section Lemmas.

      Lemma derivability_from_empty:
        ∀ w, derf G [] w → w = [].

      Lemma derivability_from_terminal:
        ∀ x y, derf G [Ts x] y → [Ts x] = y.

      Lemma derf_is_length_monotone:
        ∀ p1 p2,
          derf G p1 p2 →
          length p1 ≤ length p2.

      Lemma empty_is_not_derivable:
        ∀ r, ¬ der G r [].

      Lemma derivability_of_terminal:
        ∀ r t,
          der G r [Ts t] →
          R r [Ts t] el G.
      Lemma derivability_step:
        ∀ w1 w2 r r1 r2,
          R r [Vs r1; Vs r2] el G →
          der G r1 w1 →
          der G r2 w2 →
          @der T V G r (w1 ++ w2).

      Lemma derivability_backward_step:
        ∀ w r,
          length w ≥ 2 →
          terminal w →
          der G r w →
          ∃ r1 r2 w1 w2,
            R r [Vs r1; Vs r2] el G ∧
            der G r1 w1 ∧
            der G r2 w2 ∧
            length w1 > 0 ∧
            length w2 > 0 ∧
            w1 ++ w2 = w.
    End Lemmas.

    Section MainLemma.

      Hypothesis inductive_step_1:
        ∀ (r : _) (t : ter),
          R r [Ts t] el G →
          P r [Ts t].

      Hypothesis inductive_step_2:
        ∀ (r r1 r2: _) (w1 w2 : phrase),
          R r [Vs r1; Vs r2] el G →
          P r1 w1 →
          P r2 w2 →
          terminal w1 →
          terminal w2 →
          der G r1 w1 →
          der G r2 w2 →
          P r (w1 ++ w2).

      Lemma chomsky_derivability_induction:
        ∀ (r : _) (w : _),
          @der T V G r w →
          terminal w →
          P r w.
    End MainLemma.

  End Induction.

End ChomskyInduction.